Satisfiability modulo theories (SMT) solving and satisfiability (SAT) solving may allow a computer to reason about systems and computations symbolically. SMT and SAT solving may be used in software verification, symbolic analysis, program verification, automatic testing, security checking, and the like. SAT solving may include determining whether a model of a propositional formula exists such that the formula evaluates as TRUE. SMT solving may include SAT solving in which propositional variables of the SAT problem are replaced with formulas of another mathematical theory.
To perform satisfiability modulo theories (SMT) solving and satisfiability (SAT) solving, some methods and systems may employ the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. The DPLL algorithm is a backtracking-based search algorithm for deciding SAT of propositional logic formulae. Theory solvers may be used with the DPLL algorithm to perform SMT solving. Additional methods and systems have been developed that may improve the performance of the DPLL algorithm. For example, the DPLL may be adapted to employ backjumping, restarting, and/or clause learning.
Efficiency in SMT and SAT solving may remain a significant obstacle, however, particularly when attempting to solve increasingly large problems. For example, in nondeterministic polynomial time (NP)-complete problems, the complexity of the problems may be exponential to the number of variables in the problems. Thus, some SMT and SAT problems may not be solvable using current methods and systems.
The subject matter claimed herein is not limited to embodiments that solve any disadvantages or that operate only in environments such as those described above. Rather, this background is only provided to illustrate one example technology area where some embodiments described herein may be practiced.